Inference at * 
Iof proof for Lemma p-compose-inject:


  A, B, C:Type, g:(A(B + Top)), f:(B(C + Top)).
  p-inject(A;B;g)  p-inject(B;C;f)  p-inject(A;C;f o g  ) 

latex

 by (Auto) 
CollapseTHEN ((All (Unfold `p-inject`)) 
CollapseTHEN ((Auto) 
CollapseTHEN (((
CRWO "do-apply-compose" (-1)) 
THEN (Auto)) 
CollapseTHEN (((RepeatFor (first_nat 2:n) ((
CFLemma `can-apply-compose` [-3]) 
CollapseTHENA (Auto)))) 
CollapseTHEN (((FHyp 7 [-3]) 

CoCollapseTHENA (Auto)) 
CollapseTHEN ((FHyp 6 [-1]) 
THEN (Auto))))))) 

latex

T.

Definitions	Type, x:AB(x), left + right, Top, p-inject(A;B;f), b, s = t, {T}, P  Q, P & Q, x:A. B(x)
Lemmas	do-apply-compose, can-apply-compose